MAYBE 1.971
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:
↳ HASKELL
↳ BR
mainModule Main
| ((enumFrom :: Float -> [Float]) :: Float -> [Float]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((enumFrom :: Float -> [Float]) :: Float -> [Float]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule Main
| ((enumFrom :: Float -> [Float]) :: Float -> [Float]) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ Narrow
mainModule Main
| (enumFrom :: Float -> [Float]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(vx3100)) → new_primMulNat(vx3100)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(vx3100)) → new_primMulNat(vx3100)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ RuleRemovalProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
The TRS R consists of the following rules:
new_primPlusInt(Neg(Succ(Zero))) → Pos(Zero)
new_primPlusInt(Neg(Succ(Succ(vx30000)))) → Neg(Succ(vx30000))
new_primPlusNat(Succ(vx3000)) → Succ(Succ(new_primPlusNat0(vx3000)))
new_primPlusInt(Pos(vx300)) → Pos(new_primPlusNat(vx300))
new_primPlusNat0(Zero) → Zero
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Float(vx30, vx31)) → Float(new_primPlusInt(vx30), new_primMulInt(vx31))
new_primMulNat0(Zero) → Zero
new_primMulInt(Pos(vx310)) → Pos(new_primMulNat0(vx310))
new_primPlusNat0(Succ(vx30000)) → Succ(vx30000)
new_primMulNat0(Succ(vx3100)) → new_primPlusNat(new_primMulNat0(vx3100))
new_primMulInt(Neg(vx310)) → Neg(new_primMulNat0(vx310))
new_primPlusInt(Neg(Zero)) → Pos(Succ(Zero))
The set Q consists of the following terms:
new_primPlusInt(Neg(Succ(Succ(x0))))
new_primPlusInt(Neg(Zero))
new_primMulInt(Neg(x0))
new_ps(Float(x0, x1))
new_primPlusNat(Succ(x0))
new_primPlusInt(Pos(x0))
new_primMulNat0(Succ(x0))
new_primMulInt(Pos(x0))
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primMulNat0(Zero)
new_primPlusInt(Neg(Succ(Zero)))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
new_primPlusInt(Neg(Succ(Zero))) → Pos(Zero)
new_primPlusInt(Neg(Zero)) → Pos(Succ(Zero))
Used ordering: POLO with Polynomial interpretation [25]:
POL(Float(x1, x2)) = 2·x1 + 2·x2
POL(Neg(x1)) = 2 + 2·x1
POL(Pos(x1)) = 2·x1
POL(Succ(x1)) = x1
POL(Zero) = 0
POL(new_numericEnumFrom(x1)) = x1
POL(new_primMulInt(x1)) = x1
POL(new_primMulNat0(x1)) = x1
POL(new_primPlusInt(x1)) = x1
POL(new_primPlusNat(x1)) = x1
POL(new_primPlusNat0(x1)) = x1
POL(new_ps(x1)) = x1
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ NonTerminationProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
The TRS R consists of the following rules:
new_primPlusInt(Neg(Succ(Succ(vx30000)))) → Neg(Succ(vx30000))
new_primPlusNat(Succ(vx3000)) → Succ(Succ(new_primPlusNat0(vx3000)))
new_primPlusInt(Pos(vx300)) → Pos(new_primPlusNat(vx300))
new_primPlusNat0(Zero) → Zero
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Float(vx30, vx31)) → Float(new_primPlusInt(vx30), new_primMulInt(vx31))
new_primMulNat0(Zero) → Zero
new_primMulInt(Pos(vx310)) → Pos(new_primMulNat0(vx310))
new_primPlusNat0(Succ(vx30000)) → Succ(vx30000)
new_primMulNat0(Succ(vx3100)) → new_primPlusNat(new_primMulNat0(vx3100))
new_primMulInt(Neg(vx310)) → Neg(new_primMulNat0(vx310))
The set Q consists of the following terms:
new_primPlusInt(Neg(Succ(Succ(x0))))
new_primPlusInt(Neg(Zero))
new_primMulInt(Neg(x0))
new_ps(Float(x0, x1))
new_primPlusNat(Succ(x0))
new_primPlusInt(Pos(x0))
new_primMulNat0(Succ(x0))
new_primMulInt(Pos(x0))
new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primMulNat0(Zero)
new_primPlusInt(Neg(Succ(Zero)))
new_primPlusNat0(Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
new_numericEnumFrom(vx3) → new_numericEnumFrom(new_ps(vx3))
The TRS R consists of the following rules:
new_primPlusInt(Neg(Succ(Succ(vx30000)))) → Neg(Succ(vx30000))
new_primPlusNat(Succ(vx3000)) → Succ(Succ(new_primPlusNat0(vx3000)))
new_primPlusInt(Pos(vx300)) → Pos(new_primPlusNat(vx300))
new_primPlusNat0(Zero) → Zero
new_primPlusNat(Zero) → Succ(Zero)
new_ps(Float(vx30, vx31)) → Float(new_primPlusInt(vx30), new_primMulInt(vx31))
new_primMulNat0(Zero) → Zero
new_primMulInt(Pos(vx310)) → Pos(new_primMulNat0(vx310))
new_primPlusNat0(Succ(vx30000)) → Succ(vx30000)
new_primMulNat0(Succ(vx3100)) → new_primPlusNat(new_primMulNat0(vx3100))
new_primMulInt(Neg(vx310)) → Neg(new_primMulNat0(vx310))
s = new_numericEnumFrom(vx3) evaluates to t =new_numericEnumFrom(new_ps(vx3))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [vx3 / new_ps(vx3)]
- Semiunifier: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from new_numericEnumFrom(vx3) to new_numericEnumFrom(new_ps(vx3)).
Haskell To QDPs